{{about, automated theorem proving, the complexity class named EQP, EQP (complexity)
EQP, an abbreviation for equational prover, is an
automated theorem proving
Automated theorem proving (also known as ATP or automated deduction) is a subfield of automated reasoning and mathematical logic dealing with proving mathematical theorems by computer programs. Automated reasoning over mathematical proof was a maj ...
program for
equational logic First-order equational logic consists of quantifier-free terms of ordinary first-order logic, with equality as the only predicate symbol. The model theory of this logic was developed into universal algebra by Birkhoff, Grätzer, and Cohn. It was l ...
, developed by the Mathematics and Computer Science Division of the
Argonne National Laboratory
Argonne National Laboratory is a science and engineering research United States Department of Energy National Labs, national laboratory operated by University of Chicago, UChicago Argonne LLC for the United States Department of Energy. The facil ...
. It was one of the provers used for solving a longstanding problem posed by
Herbert Robbins
Herbert Ellis Robbins (January 12, 1915 – February 12, 2001) was an American mathematician and statistician. He did research in topology, measure theory, statistics, and a variety of other fields.
He was the co-author, with Richard Courant ...
, namely, whether all
Robbins algebra
In abstract algebra, a Robbins algebra is an algebra containing a single binary operation, usually denoted by \lor, and a single unary operation usually denoted by \neg. These operations satisfy the following axioms:
For all elements ''a'', ''b'', ...
s are
Boolean algebra
In mathematics and mathematical logic, Boolean algebra is a branch of algebra. It differs from elementary algebra in two ways. First, the values of the variables are the truth values ''true'' and ''false'', usually denoted 1 and 0, whereas in e ...